The subject matter disclosed herein relates to circuit verification and more particularly relates to integrated circuit design model splitting for formal verification.
Formal verification is a method of determining if logic of a circuit has any errors or bugs. Formal verification is implemented by converting a design of an integrated circuit (“IC”) into a simpler “verifiable” format. A typical design is specified as set of interacting systems where each system has a finite number of states. States and transitions between states may constitute finite state machines (“FSMs”). A circuit can be represented by representing each component in terms of a present state (or current configuration) and a next state (or successive configuration). The circuit may be represented by discrete functions, which may be represented in a binary decision diagram (“BDD”), which is a data structure that represents Boolean functions and/or a multi-valued decision diagram (“MDD”), which is a data structure that represents finite valued discrete functions. Components of an integrated circuit diagram may be placed in a netlist, which includes a list of components, nodes or connection points of the components, and possibly attributes of the components involved. In one embodiment, the netlist includes sufficient information to transform the netlist into BDDs, MDDs or other logic structure useful for formal verification. Other formal verification methods may use satisfaction-based (“SAT-based”) state enumeration.
Algorithms for checking for design errors in the integrated circuit design are often called engines or algorithm engines and use a netlist along with user constraints, initial conditions, etc. for determining is design errors are present, which may be called “reachability analysis.” A design error, such as an inverter with an input and an output that are a same value, are considered to be bugs. Formal verification uses one or more engines to determine if design errors or bugs are present in the integrated circuit design.
Often a netlist is complex enough to require exorbitant computational resources so execution of one or more engines may take days or weeks, or may take a large amount of memory, etc. In general, there is no clear dependency between the structure or size of an analyzed circuit and required resources. However, a smaller number of registers, gates, arrays, etc. often results in increased computational performance. Transformation-based verification (“TBV”) is a form of formal verification where some engines are used to simplify a netlist by reducing redundant gates, inputs, registers, arrays, constraints, etc. so that a resultant modified netlist may be used that requires less computational resources and/or executes in less time. Multiple engines may be used for processing a netlist where each engine has different characteristics. For example, some engines may be good at reducing inputs while other engines may be good at reducing registers, other engines may be good at reducing AND gates, other engines may excel at verifying there are no design errors for a particular netlist or components in the netlist, etc. Some formal verification computer programs may have access to thirty or more engines.
One method of formal verification of a complex netlist of an integrated circuit design includes splitting the design. However, manually splitting the design results in arbitrary splits and may result in stages where a sub-proof is not possible.